package dbc;

import java.io.IOException;
import java.io.PrintWriter;
import java.util.List;
import java.util.Set;
import javax.annotation.processing.AbstractProcessor;
import javax.annotation.processing.Filer;
import javax.annotation.processing.RoundEnvironment;
import javax.annotation.processing.SupportedAnnotationTypes;
import javax.annotation.processing.SupportedSourceVersion;
import javax.lang.model.SourceVersion;
import javax.lang.model.element.Element;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.Modifier;
import javax.lang.model.element.TypeElement;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.Types;
import javax.tools.Diagnostic.Kind;
import javax.tools.StandardLocation;

/**
* PostProcessor is called at compilation time to process
* all @Post annotations in the source code.
* For each method annoted with @Post, this processor will create
* an aspect per method which will have to be compile with aspectj.
*/
// PostProcessor supports only @Post annotations
@SupportedAnnotationTypes({"dbc.Post"})
// Only Java >= 6 is supported
@SupportedSourceVersion(SourceVersion.RELEASE_6)
public class PostProcessor extends AbstractProcessor {
    /**
     * Process is called during compilation to parse all @Invariant annotations
     * @param annotations A set containing all @Invariant annotations
     * @param roundEnv Object representating the current step of annotations processing
     * @return true on success
     */
    @Override
    public boolean process(Set<? extends TypeElement> annotations, RoundEnvironment roundEnv) {
	// Creating ressources for output resulting file    
        Filer filer = processingEnv.getFiler();
        Types types = processingEnv.getTypeUtils();

	// Get all Elements (here methods) annoted with @Post
	// Each Element will be process to create an aspect
        for(Element element : roundEnv.getElementsAnnotatedWith(Post.class)) {
            try {
		// Getting usefull informations such as class name to generate an unique aspect name
                TypeMirror classType = element.getEnclosingElement().asType();

                String className = classType.toString();
                String erasedClassName = types.erasure(classType).toString();

                String methodName = element.getSimpleName().toString();

                String aspectName = "PostAspect_" + erasedClassName + "_" + methodName;
                aspectName = aspectName.replace(".", "_");

                PrintWriter pw = new PrintWriter(
                        filer.createResource(StandardLocation.SOURCE_OUTPUT,
                                             "aspects", aspectName + ".aj")
                                             .openOutputStream());

                boolean isStatic = element.getModifiers().contains(Modifier.STATIC);

                ExecutableElement exec = (ExecutableElement) element;

                String paramNames = "";
                String paramList = "";
                String erasedParamTypes = "";
                String erasedParamList = "";
		// Get all method's parameters and paramters' name
                for(VariableElement param : exec.getParameters()) {
                    TypeMirror type = param.asType();
                    String name = param.getSimpleName().toString();

                    if(!paramList.isEmpty()) {
                        paramNames += ", ";
                        paramList += ", ";
                        erasedParamTypes += ", ";
                        erasedParamList += ", ";
                    }

                    paramNames += name;
                    paramList += type + " " + name;
                    erasedParamTypes += types.erasure(type);
                    erasedParamList += types.erasure(type) + " " + name;
                }

		// Here we have the post annotation
                Post post = element.getAnnotation(Post.class);
		// Analyze post annotation to handle special operators such as $old
                PostConditionHandler pch = new PostConditionHandler(post.value(), erasedClassName, methodName,
                                                                    erasedParamList, isStatic);
                pch.processExpression();
                String condition = pch.getProcessedExpression();


                List<String> olds = pch.getOldVariableNames();
                String oldList = "";
                String oldNames = "";

                for(String oldName : olds) {
                    if(!oldList.isEmpty()) {
                        oldList += ", ";
                        oldNames += ", ";
                    }

                    oldList += "Object " + oldName;
                    oldNames += oldName;
                }


                boolean returnsValue = (exec.getReturnType().getKind() != TypeKind.VOID);
                String returnType = types.erasure(exec.getReturnType()).toString();
                String returnVariableName = PostConditionHandler.RETURN_VARIABLE_NAME;
                String returnDeclaration = returnType + " " + returnVariableName;


                //Aspect generation
                pw.println("privileged aspect " + aspectName + " implements dbc.Contract {");

                pw.println(pch.getGeneratedAspectCode());

                pw.print("private ");
                if(isStatic) pw.print("static ");
                pw.print("void " + erasedClassName + ".postAssert"+methodName+"(");

                pw.print(StringUtils.concatNonEmpty(", ", (returnsValue ? returnDeclaration : ""),
                                                    erasedParamList, oldList));
                pw.println(") {");

                pw.println(pch.getGeneratedCode());
                
                pw.println("if(!(" + condition + ")) {");
                pw.print("throw new dbc.PostConditionException(\"Postcondition violated in ");
                pw.println(className + "." + methodName + "(" + paramList + ")\");");
                pw.println("}");
                pw.println("}");

                pw.print(returnType + " around(" + erasedParamList + "): ");
                pw.print("call(" + returnType + " " + erasedClassName + "." + methodName + "(" + erasedParamTypes + "))");
                pw.println(" && args(" + paramNames + ") && !within(dbc.Contract+) {");

                String reference = isStatic ? erasedClassName
                                            : ("((" + erasedClassName + ")thisJoinPoint.getTarget())");

                for(String oldName : olds) {
                    pw.println("Object " + oldName + " = " + reference + "." + oldName + methodName + "(" + paramNames + ");");
                }

                if(returnsValue) {
                    pw.print(returnDeclaration + " = ");
                }

                pw.println("proceed(" + paramNames + ");");

                pw.print(reference + ".postAssert"+methodName+"(");
                pw.print(StringUtils.concatNonEmpty(", ", (returnsValue ? returnVariableName : ""),
                                                    paramNames, oldNames));
                pw.println(");");

                if(returnsValue) {
                    pw.println("return " + returnVariableName + ";");
                }
                pw.println("}}");

                pw.close();


            } catch(IOException ex) {
		// If something goes wrong display a warning and return
                processingEnv.getMessager().printMessage(Kind.WARNING, ex.getMessage());
            }
        }

        return true;
    }
}
